\section{Syntax}

\begin{definition}[Syntax]

$$
\begin{array}{lclr}
P & ::= & \\
  	&& c(x:\capab).P \sepr \outC{c}{v}.P & \text{I/O}\\
	&& \component{l}{h}{P} \sepr \update{l}{X}{\Delta}{U} & \text{Adaptable processes}\\
	&& \open{c:\rho}.P & \text{Open}	\\
	&& \close{c}.P & \text{Close}	\\	
	&& P \parallel P \sepr \restr{c}{P} & \text{Constructs}\\	
	&& \ifte{x=v}{P}{P} & \text{Conditional}\\
	&& \branch{c}{n:P \dots n:P} \sepr \select{c}{n}.P & \text{Branch and Select}\\
	\\
U	&::= & P_X &\text{Update}
	
\end{array}
$$

\end{definition}

(For the moment) restriction should not be used as a "real" construct. Processes do not make use of restriction that is only introduced by the semantics.

\section{Semantics}

\begin{definition}[Structural congruence]
$$
\begin{array}{c}
P \parallel Q \equiv Q \parallel P \\
(P \parallel Q) \parallel R \equiv P \parallel (Q \parallel R)\\
P \parallel \nil \equiv P \\
\restr{a}{P} \parallel Q \equiv \restr{a}{P \parallel Q}\\
\restr{a}{\nil} \equiv \nil\\
\restr{a}{\restr{b}{P}} \equiv \restr{b}{\restr{a}{P}}\\
\restr{a}{\component{l}{h}{P}} \equiv \component{l}{h}{\restr{a}{P}}
\end{array}
$$

\end{definition}



\begin{definition}[Nesting Context]
This is used to represent the fact that interacting parts can be arbitrarily nested inside locations

$$
C ::= \bullet \sepr C \parallel P  \sepr \restr{c}C \sepr \component{l}{h}{C}
$$
\end{definition}

\begin{definition}
How to increase/decrease safe sessions in contexts $C^{+h}$:
$$
\begin{array}{lcl}
(\bullet)^{+h} & ::= & \bullet \\
(C \parallel P)^{+h} & ::= & C^{+h} \parallel P \\
(\component{l}{k}{C})^{+h} & ::= & \component{l}{{k+h}}{C^{+h}} \\
(\restr{c}{C})^{+h} & ::= & \restr{c}{C^{+h}}


\end{array}
$$
\end{definition}


\begin{definition}[Reduction rules]

-- Nota su regola upd: se il controllo della conformita' del tipo della location non si fa in questo punto vuol dire che a run time posso avere sia evoluzioni ben tipate che evoluzioni non ben tipate. Non posso spostare questo controllo nell'operatore $\bowtie$ perche' non e' binario e non e' invariante.


-- Notice that the same adaptable process can be updated by a number of updates. This way, as for the open rule, we must check also in the semantics that only the good components are updated. This check cannot be done by the typing system because it would be too restrictive. I.e. at any time you require that all the updates could be performed on every component


$$
\begin{array}{lr}

\restr{c}{E[C[c(x:\capab).P] \parallel D[\outC{c}{v}.R]]} \pired \\
\qquad \restr{c}{E[C[P\sub{v}{x}] \parallel D[R]]} & \rulename{r:I/O} \\
\\



E[C[\open{c:\rho}.P] \parallel D[\open{d:\overline{\rho}}.R]] \pired \\
\qquad \restr{c'}{E^{+1}[{C^{+1}[P\sub{c'}{c}] \parallel D^{+1}[R]\sub{c'}{d}}]} & \rulename{r:Open} \\
\\


\restr{cd}{E[C[\close{c}.P] \parallel D[\close{d}.R]]} \pired \\
\qquad \restr{cd}{E^{-1}[C^{-1}[P] \parallel D^{-1}[R]]} & \rulename{r:Close} \\
\\


E[C[\component{l}{0}{P}] \parallel D[\update{l}{x}{\Delta}{U}.R]] \pired E[C[U\sub{P}{x}] \parallel D[R]] & \rulename{r:Upd}\\
%
%\cfrac{\forall (c:\rho) \in \Delta, \open{c:\rho} \in P ~or~ P\propto\Delta }{E[C[\component{l}{0}{P}] \parallel D[\update{l}{x}{\Delta}{U}.R]] \pired E[C[U\sub{P}{x}] \parallel D[R]]} & \rulename{r:Upd} \\
\\


C[\ifte{v=v}{P}{Q}] \pired C[P] & \rulename{r:IfTr} \\
\\


C[\ifte{u=v}{P}{Q}] \pired C[Q]  \quad (\text{with } u \neq v)& \rulename{r:IfFa} \\
\\

\restr{c}{E[C[\branch{c}{n_i:P_i}_{i\in I}] \parallel D[\select{c}{n_j}.R]]} \pired \\
\qquad \restr{c}{E[C[P_j] \parallel D[R]]} & \rulename{r:Branch} \\
\\

\cfrac{P \equiv P' \qquad P' \pired Q' \qquad Q \equiv Q'}{P \pired Q} & \rulename{r:Str}\\
\\

\cfrac{P \pired P' }{P\parallel Q \pired P' \parallel Q} & \rulename{r:Par}\\
\\

\cfrac{P \pired P' }{\restr{c}{P} \pired \restr{c}{P'}} & \rulename{r:Res}
\end{array}
$$

\end{definition}


\section{Types}
Definire tipo duale


\begin{definition}[Types syntax]

Basic types
$$
\begin{array}{lclr}
\capab & ::= & \mathrm{int} \sepr \mathrm{real} \sepr \dots & \text{channel capabilities}\\

\varphi & ::= & \var & \text{process variable}
\end{array}
$$

Session types (notice that you need to add presession types when using recursive types)
$$
\begin{array}{lclr}
\rho &::= & \epsilon & \text{closed session}\\
		&& !\capab.\rho & \text{send type} \\ 
		&& ?\capab.\rho & \text{receive type} 
\end{array}
$$

Channels types
$$
\begin{array}{lclr}
\omega &::=& \rho & \text{session}\\
	&&	\bot & \text{used session}
\end{array}
$$

Environments
$$
\begin{array}{lclr}
\Phi & ::= & \emptyset \sepr \Phi, c:\omega & \text{process interface}\\
\Gamma &::= & \emptyset \sepr \Gamma, v:\capab & \text{first order environment }\\
\Theta &::= & \emptyset \sepr \Theta, X:\varphi & \text{higher order environment }\\
\end{array}
$$
\end{definition}

A \emph{type judgment} is of form: 
$$\Gamma ; \Theta \vdash P : \Phi $$ where $\Gamma$ is a first order environment mapping names and channels (when we add values here we will put also capabilities of channels), $\Theta$ is a higher order environment storing process variable (for the moment this variables do not have any "special value", but i think that this should be the place where to put a particular type for checking consistency of updates: an update can take place only if the updated process has the same type of the former process).

\begin{definition}[Merge]

$$
\begin{array}{lcl}
\Phi_1 \bowtie \Phi_2 &=& \{ c:\omega_1 \bowtie \omega_2 \mid c:\omega_1 \in \Phi_1 \text{ and } c:\omega_2 \in \Phi_2\} \cup \\
&&\{ c:\omega_1 \mid c:\omega_1 \in \Phi_1 \text{ and } c\notin \dom{\Phi_2}\} \cup\\
&&\{ c:\omega_2 \mid c:\omega_2 \in \Phi_2 \text{ and } c\notin \dom{\Phi_1}\}
\end{array}
$$
and
$$
\omega_1 \bowtie \omega_2 = 
\begin{cases}
\bot & \text{if } \{\omega_1, \omega_2\} = \{ \rho , \overline{\rho}\}\\
undefined & \text{otherwise}
\end{cases}
$$
\end{definition}

\begin{definition}[Typing rules -- Well formed processes]
$$
\begin{array}{lr}

\cfrac{}{\Gamma, x:\capab \vdash x:\capab} & \rulename{Cap}\\

\cfrac{}{\Theta,X:\var \vdash X:\var} & \rulename{Proc-var}\\

\cfrac{}{\Gamma;\Theta \vdash \nil:\emptyset} & \rulename{Nil}\\
\\

\cfrac{\Gamma;\Theta \vdash P : \Phi, c:\rho}{\Gamma; \Theta \vdash \open{c:\rho}.P : \Phi} & \rulename{Open}\\
\\

\cfrac{\Gamma;\Theta \vdash P : \Phi \qquad c\notin \dom{\Phi} }{\Gamma; \Theta \vdash \close{c}.P : \Phi, c:\epsilon} & \rulename{Close}\\
\\

\cfrac{\Gamma, x:\capab;\Theta \vdash P : \Phi, c:\rho}{\Gamma; \Theta \vdash c(x:\capab).P : \Phi, c:?\capab.\rho} & \rulename{Receive}\\
\\


\cfrac{\Gamma;\Theta \vdash P : \Phi, c:\rho \qquad \Gamma \vdash v : \capab}{\Gamma; \Theta \vdash \outC{c}{v}.P : \Phi, c:!\capab.\rho} & \rulename{Send}\\
\\
%
%\cfrac{\Gamma;\Theta \vdash P : \Phi \qquad c\notin \dom{\Phi} }{\Gamma; \Theta \vdash P : \Phi, c:\bot} & \rulename{Weak}\\
%\\

\cfrac{\Gamma;\Theta \vdash P : \Phi, c:\bot }{\Gamma; \Theta \vdash \restr{c}{P} : \Phi, c:\bot} & \rulename{Restr}\\
\\

\cfrac{\Gamma;\Theta \vdash P : \Phi_1 \qquad \Gamma;\Theta \vdash Q : \Phi_2 \qquad \Phi = \Phi_1 \bowtie \Phi_2 }{\Gamma; \Theta \vdash P \parallel Q : \Phi} & \rulename{Par} \\
\\

\cfrac{\Gamma;\Theta \vdash P : \Phi \qquad n = \#\{c \mid c:\omega \in \Phi\} }{\Gamma; \Theta \vdash \component{l}{n}{P} : \Phi} & \rulename{Loc} \\
\\

\cfrac{\Gamma; \Theta,X:\var \vdash U: \emptyset}{\Gamma; \Theta \vdash \update{l}{X}{\Delta}{U} : \emptyset} & \rulename{Update} \\
\\

\cfrac{\Gamma; \Theta \vdash P : \Phi \quad \Gamma; \Theta \vdash Q : \Phi \quad \Gamma \vdash u:\capab \quad \Gamma \vdash v:\capab}{\Gamma; \Theta \vdash \ifte{u=v}{P}{Q} : \Phi} & \rulename{Condit}\\
\\

\cfrac{\forall i\in I \ \Gamma; \Theta \vdash P_i : \Phi, c:\rho_i \quad \rho = \&\{n_1:\rho_1 \vee \dots \vee n_k:\rho_k \}}{\Gamma; \Theta \vdash \branch{c}{n:P \dots n:P} : \Phi, c:\rho} & \rulename{Branch}\\
\\

\cfrac{ \Gamma; \Theta \vdash P : \Phi, c:\rho_i \qquad \rho = \oplus\{n_1:\rho_1 \vee \dots \vee n_k:\rho_k \}}{\Gamma; \Theta \vdash \select{c}{n_i}.P : \Phi, c:\rho} & \rulename{Select}
\end{array}
$$


\end{definition}




\section{Varius Comments}
\begin{enumerate}
	\item Per il momento ho messo comunicazione alla CCS, pensare se aggiungere pi communication come in Vasconcelos
	\item se non si spedisce valori, non ha senso avere un operatore if then else
	\item pensare se il calcolo avrebbe piu' o meno senso, impedendo di eliminare locations	
	\item Note that all adaptable processes inside an update context must have their safe session number set to 0!!! In realta' e' il tipo a occuparsi di questo, mi basta assicurare che il numero corrisponda alle sessioni aperte
	\item ATTENZIONE la regola \rulename{Loc red} crea un problema: se inclusa si rischia di non aggiornare le sessioni aperte al momento di una open (e simmetricamente di non chiuderle in caso di una close) questo comporta che in tutte le reduction rules ci si debba ricordare il nesting delle location fino a top level (ruolo di E), da questa osservazione deriva anche la giustificazione della definizione di nesting context
	$$
	\cfrac{P \pired P' }{\component{l}{n}{P} \pired \component{l}{n}{P'}} \qquad \rulename{Loc red}\\
	$$

	\item Ci sono diverse decisioni da prendere sulla open reduction: 
	
	1) si puo' seguire uno stile alla dezani prima versione o alla vasconcelos seconda versione in cui si chiede che il link cd sia gia' stato creato
	
	2) sempre riguardo alle locations: io ho tolto il requirement per cui la open doveva avvenire in due locations con lo stesso nome, questo ci permette anche di avere open locali alla stessa location
	
	
	\item per le regole di tipo, mi serve un binder nell'update, per ora ho messo questo $\lambda x.U$ probabilmente ci sono notazioni migliori
	
	\item attenzione per ora non ho messo la ricorsione, ma non dovrebbe cambiare niente, rispetto alle solite regole di tipaggio
	
	\item Non so se ha tanto senso controllare che c sia un canale nella rule close, idem la rule loc name non mi convince , al massimo farei come per channel un controllo l in nomi
\end{enumerate}
